A:Type, I:MaInterface(A), i:{i:Id| (i  fpf-domain(I))} , k:{k:Knd| (k  fpf-domain(I(i).2))} .
(k  ma-interface-kinds(I)) 

latex

Definitions

Id, t  T, {x:A| B(x)} , Knd, b, Top, left + right, x:AB(x), x:A. B(x), State(ds), Type, x:A  B(x), hasloc(k;i), x. t(x), a:A fp B(a), x.A(x), Atom$n, MaInterface(T), (x  l), f(x), t.1, t.2, type List, P  Q, ma-interface-kinds(I), fpf-domain(f), False, A, P  Q, Dec(P), map(f;as), P  Q, P & Q, P  Q, #$n, ||as||, a < b, Void, A  B, , , l[i], s = t, A c B, , IdLnk, x:A. B(x), IdDeq, x  dom(f), if b then t else f fi , S  T

Lemmas

l member-set, list-set-type, list-subtype, member map, length wf nat, ma-interface-kinds-aux2, member-fpf-domain, IdLnk wf, nat wf, length wf1, select wf, ma-interface-kinds-aux1, member-concat, ma-interface-kinds-aux0, decidable equal Id, decidable l member, decidable equal Kind, l member wf, fpf-domain wf, ma-interface wf, l member subtype, pi2 wf, fpf-trivial-subtype-top, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf, Id wf